Nuprl Definition : ma-ef-val 0,22

M.ef(k,x,s,v)?w == 1of(2of(2of(2of(2of(M)))))(<k,x>)?s,vw(s,v
latex



clarification:

M.ef(k,x,s,v)?w
== fpf-cap(1of(2of(2of(2of(2of(M)))));product-deq(Knd;Id;KindDeq;IdDeq);<k,x>;s,vw)(s,v
latex


DefinitionsM.ef(k,x,s,v)?w, f(x)?z, 1of(t), 2of(t), product-deq(A;B;a;b), Knd, Id, KindDeq, IdDeq
FDL editor aliasesma-ef-val

origin